Inference at * 
Iof proof for Lemma fincr wf2:


  FIncr  Type 

latex

 by Unfold `fincr` 0 

latex

 1: 

 1:   {f | i:  if (i = 0) then  else {f(i - 1)...} fi }  Type
 .

Definitions

FIncr